(declare-fun id_ds1_filter_init () (Array Int (Array Int Real)))
(declare-fun a () Real)
(declare-fun h () (Array Int (Array Int Real)))
(declare-fun pv63 () Int)
(declare-fun g () (Array Int (Array Int Real)))
(declare-fun i (Int Real) (Array Int Real))
(assert (forall ((?k Int) (?j Real)) (= (select (i 0 ?j) ?k) ?j)))
(assert (not (=> (forall ((?b Int) (?c Int)) (=> (>= ?b 0) (<= ?b 5) (= (select (select g ?b) ?c) a))) (forall ((?l Int) (?d Int)) (=> (>= ?d 5) (= (select (select h ?l) ?d) a))) (forall ((?m Int) (?n Int)) (let ((?e 0)) (= (and (>= ?m ?e)) (= (< ?m pv63) (= (select (select id_ds1_filter_init ?m) ?n) a))))) (forall ((?o Int) (?f Int)) (=> (>= ?o 0) (<= ?o 2) (<= ?f 2) (= 0 a))))))
(check-sat)
